Step of Proof: complete_nat_ind 9,38
Inference at * 1 
Iof proof for Lemma complete nat ind:



1. P : {k}
2. i:. (j:i. P(j))  P(i)
3. i : 
  P(i) 
latex
 by InteriorProof ((NCompInd 3) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 2:n
CollapseTHENA ((Au),(first_nat 3:n)) (first_tok :t) inil_term))) 
latex

C1: 

C1: 4. i1:i. P(i1)
C1:   P(i)
C.

Definitionst  T, False, A, A  B, i  j , P  Q, x:A. B(x), , , P  Q, i  j < k, {i..j}
Lemmasnat properties, int seg wf, le wf, ge wf, nat wf

origin